Inference at * 1 1 
Iof proof for Lemma minus functionality wrt le:



1. i : 
2. j : 
3. j  i
  (-i)  (-j) 

latex

 by (RA ((Assert (-(i+j))  (-(i+j))) 
CollapseTHENM (
CFwdThruLemma `add_functionality_wrt_le` [3;-1]))) 

latex

C.

Definitions	t  T, False, P  Q, A, A  B, x:A. B(x)
Lemmas	add functionality wrt le